
#use "hol.ml";;

1 + 1;;
let rec fact n = if n = 0 then 1 else n * fact (n-1);;

(* -------------------------------------------------------------------------- *)
(*  Terms                                                                     *)
(* -------------------------------------------------------------------------- *)

`x + 1`;;
"x + 1";;

#remove_printer print_qterm;;

`x + 1`;;

#install_printer print_qterm;;

`x + 1`;;

subst [`2`,`1`] `x + 1`;;
subst [`y + 2`,`x:num`] `x + 5 * x`;;

(* -------------------------------------------------------------------------- *)
(*  Types                                                                     *)
(* -------------------------------------------------------------------------- *)

`:num`;;
type_of `1`;;
type_of `x + 1`;;
type_of `x + 1 < x + 2`;;

`x`;;
`x:num`;;
`x:bool`;;
`(x:num) = y`;;
`(x:num) + 1`;;

`(x < y) + 2`;;

`(x:num) + (y:real)`;;

(* -------------------------------------------------------------------------- *)
(*  Theorems                                                                  *)
(* -------------------------------------------------------------------------- *)

`x + 1 < x + 2`;;
`2 + 2 = 5`;;

REFL `x:real`;;
let th1 = REFL `x + 1`;;
let th3 = INST [`2`,`x:num`] th1;;

ASSUME `2 + 2 = 5`;;
let th2 = ASSUME `2 * n = n + n`;;

INST [`2`,`n:num`] th2;;
INST [`2`,`2 * n`] th2;;
concl;;
concl th1;;
dest_thm th1

(* -------------------------------------------------------------------------- *)
(*  Derived Rules                                                             *)
(* -------------------------------------------------------------------------- *)

ARITH_RULE
`(a * x + b * y + a * y) EXP 3 + (b * x) EXP 3 +
(a * x + b * y + b * x) EXP 3 + (a * y) EXP 3 =
(a * x + a * y + b * x) EXP 3 + (b * y) EXP 3 +
(a * y + b * y + b * x) EXP 3 + (a * x) EXP 3`;;

(* -------------------------------------------------------------------------- *)
(*  Propositional Logic                                                       *)
(* -------------------------------------------------------------------------- *)

p q
T
F
p ==> q
p /\ q
p \/ q
p <=> q
~ p

`p \/ ~p`;;
ASSUME `p /\ q`;;
`x < 1 ==> p`;;
ARITH_RULE `x < y \/ y <= x`;;

infixes();;
get_infix_status "==>";;
get_infix_status "-";;
get_infix_status "+";;
get_infix_status "==>";;

(* -------------------------  Proving Tautologies  -------------------------- *)

TAUT `p \/ ~p`;;
TAUT `(p <=> q) <=> (p ==> q) /\ (q ==> p)`;;
TAUT `~(p /\ q) <=> ~p \/ ~q`;;
TAUT `~(p \/ q) <=> ~p /\ ~q`;;
TAUT `(p <=> (q <=> r)) <=> ((p <=> q) <=> r)`;;
TAUT `(p ==> q) \/ (q ==> p)`;;
TAUT `((p ==> q) ==> p) ==> p`;;
TAUT `p \/ q ==> p /\ q`;;
TAUT `x < 1 /\ y > 0 ==> x < 1`;;
TAUT `0 < x /\ x < 7 ==> 1 <= x /\ x <= 6`;;
ARITH_RULE `0 < x /\ x < 7 ==> 1 <= x /\ x <= 6`;;
ARITH_RULE `x EXP n + y EXP n = z EXP n /\ n >= 3 ==> x = 0 \/ y = 0`;;

(* -----------------------  Low-level logical rules  ------------------------ *)

let thp = ASSUME `p:bool`;;
let thq = ASSUME `q:bool`;;
let thpq = CONJ thp thq;;
CONJUNCT1 thpq;;
CONJUNCT2 thpq;;

let th1 = ARITH_RULE `x <= y ==> x < y + 1`;;
let th2 = ASSUME `x <= y`;;
MP th1 th2;;



